es:ES{i}, A:Type{i}, l:IdLnk, tg:Id, ds:x:Id fp Type{i},
conds:k:Knd fp V:Type{i}  (State(ds)V(A + Top)).
sender-glues-triggers-p(es; A; l; tg; ds; conds)  {i'} 

latex

Definitions

x:A. B(x), t  T, , sender-glues-triggers-p(es; A; l; tg; ds; conds), P & Q, A c B, x. t(x), a:A fp B(a), Knd, State(ds), Top, P  Q, x:A. B(x), state@i, SQType(T), {T}, T, True, x(s), es-triggers-params-consistent(es;A;i;ds;conds), E(X), SqStable(P), P  Q, P  Q, fpf-domain(f)

Lemmas

fpf wf, Knd wf, decl-state wf, top wf, Id wf, IdLnk wf, event system wf, es-triggers-params-consistent wf, lsrc wf, es-E wf, es-kind wf, rcv wf, es-valtype wf, glues wf, es-triggers wf, assert wf, fpf-dom wf, es-in-port wf, outl wf, pi2 wf, fpf-ap wf, es-state-when wf, subtype rel dep function, es-vartype wf, es-loc wf, subtype rel self, es-E-interface wf, subtype rel product, l member wf, subtype rel function, subtype rel sum, es-sender wf, Id sq, sq stable from decidable, Kind-deq wf, fpf-trivial-subtype-top, decidable assert, es-is-interface-triggers, es-state wf, member-fpf-dom, sq stable subtype rel, fpf-cap wf, id-deq wf, es-state-subtype-iff, fpf-domain wf, exists functionality wrt iff, member-fpf-domain, es-val wf, isl wf, es-isrcv wf, es-is-interface-in-port, es-kind-rcv